﻿/*============================================
 * 类名 :ResultProve
 * 描述 :从结果出发进行推理
 *   
 * 创建时间: 2011/2/16 11:52:48
 * Blog:   http://home.cnblogs.com/xiangism
 *============================================*/
using System;
using System.Collections.Generic;

using System.Text;

namespace 命题证明
{
    /// <summary>从结果出发进行推理</summary>
    class ResultProve
    {
        ProveWork prove = new ProveWork();
        public List<ProveNode> conditions = new List<ProveNode>();
        Expression result;
        List<ProveNode> results = new List<ProveNode>();

        public List<ResultParameter> Prove( List<string> con, string r )
        {
            SetCondition( con );
            SetResult( r );
            prove.SetConditions( conditions );
            Prove( result.Head );
            ProveNode n = ProofEqual();
            if ( n != null )
            {
                ProveNode temp = n;
                ProveNode p = temp;
                string t1 = temp.ProveName;
                string t2 = "";
                temp = temp.Previous[0];
                p = p.Previous[0];
                bool isBreak = false;
                while ( true )
                {
                    if ( p.Previous.Count != 0 )
                    {
                        p = p.Previous[0];
                    }
                    else
                    {
                        isBreak = true;
                    }

                    t2 = temp.ProveName;
                    temp.ProveName = t1;
                    t1 = t2;
                    if ( temp.Previous.Count == 0 )
                    {
                        temp.Previous.Add( n.Result.Head.Tag );
                    }
                    else
                        temp.Previous[0] = n.Result.Head.Tag;
                    n.Result.Head.Tag = temp;
                    temp = p;
                    if ( isBreak )
                        break;
                }
                CreateProveProcess c = new CreateProveProcess();
                return c.CreateProcess( n.Result.Head.Tag ); // CreateProveProcess.CreateProcess( n.Result.Head.Tag );
            }
            if ( result.Head.Tag != null )
            {
                CreateProveProcess c = new CreateProveProcess();
                return c.CreateProcess( result.Head.Tag );
            }
            return null;
        }

        /// <summary>关键在这个函数，将推理节点的结果存储在Node的Tag属性中</summary>
        void Prove( Node result )
        {
            ProveNode o = prove.Work( result );
            if ( o != null )
            {
                result.Tag = o;
            }
            if ( result is OperatorNode && ( result as OperatorNode ).Operator == Operator.Or )
            {
                Prove( result.Left );
                if ( result.Left.Tag != null )
                {
                    List<ProveNode> ps = new List<ProveNode>();
                    ps.Add( result.Left.Tag );
                    ProveNode r = new ProveNode( new Expression( ExpressionFactory.ConvertToMiddle( result ) ) ) { ProveName = "附加律", Previous = ps };
                    result.Tag = r;
                    return;
                }
                Prove( result.Right );
                if ( result.Right.Tag != null )
                {
                    List<ProveNode> ps = new List<ProveNode>();
                    ps.Add( result.Right.Tag );
                    ProveNode r = new ProveNode( new Expression( ExpressionFactory.ConvertToMiddle( result ) ) ) { ProveName = "附加律", Previous = ps };
                    result.Tag = r;
                    return;
                }
            }
            else if ( result is OperatorNode && ( result as OperatorNode ).Operator == Operator.And )
            {
                Prove( result.Left );
                Prove( result.Right );
                if ( result.Left.Tag != null && result.Right.Tag != null )
                {
                    List<ProveNode> ps = new List<ProveNode>();
                    ps.Add( result.Left.Tag );
                    ps.Add( result.Right.Tag );
                    ProveNode r = new ProveNode( new Expression( ExpressionFactory.ConvertToMiddle( result ) ) ) { ProveName = "合取", Previous = ps };
                    result.Tag = r;
                    return;
                }
            }
            else if ( result is OperatorNode && ( result as OperatorNode ).Operator == Operator.Prove )
            {
                Prove( result.Left ); //todo:加入非符号
                Prove( result.Right );
                OperatorNode head = new OperatorNode( Operator.Or );
                OperatorNode no = new OperatorNode( Operator.Not );
                no.Right = result.Left;
                head.Left = no;
                head.Right = result.Right;
                ProveNode r = new ProveNode( new Expression( ExpressionFactory.ConvertToMiddle( head ) ) ) { ProveName = "", Previous = null };
            }
            else
            {
                result.Tag = prove.Work( result );
            }

        }

        ProveNode ProofEqual()
        {
            foreach ( ProveNode n in results )
            {
                Prove( n.Result.Head );
                if ( n.Result.Head.Tag != null )
                    return n;
            }
            return null;
        }

        void SetCondition( List<string> con )
        {
            conditions.Clear();
            int previous = 0;
            foreach ( string s in con )
            {
                try
                {
                    conditions.Add( new ProveNode( new Expression( s ) ) );
                }
                catch ( ExpressionException value )
                {
                    //哈，终于用到了一个重新抛出异常的例子
                    throw new ExpressionException( previous + value.Index, "条件中出现错误：" + value.Message );
                }
                previous += s.Length + 1;
            }
        }

        void SetResult( string p )
        {
            try
            {
                result = new Expression( p );
                CreateResult( new ProveNode( result ) );
            }
            catch ( ExpressionException value )
            {
                throw new ExpressionException( value.Index, "结论中出现错误：" + value.Message );
            }
        }

        void CreateResult( ProveNode node )
        {
            for ( int j = 0; j < node.Result.OperatorNodes.Count; j++ )
            {
                Expression exp = new Expression( ExpressionFactory.ConvertToMiddle( node.Result.OperatorNodes[j] ) );
                MatchLaw m = new MatchLaw();
                for ( int i = 0; i < Math.Pow( 2, exp.OperatorNodes.Count ); i++ )
                {
                    ReplaceWork replace = new ReplaceWork( exp );
                    replace.Replace( i );
                    CreateResult( m.MatchEqual( replace, new List<ProveNode>() { node } ), node.Result, j );
                }
            }
        }

        private void CreateResult( List<ProveNode> list, Expression old, int j )
        {
            foreach ( ProveNode n in list )
            {
                Expression exp = old.Clone();
                if ( exp.OperatorNodes[j].Parent == null )
                {
                    exp.Head = n.Result.Head;
                }
                else if ( exp.OperatorNodes[j].Parent.Left == exp.OperatorNodes[j] )
                {
                    exp.OperatorNodes[j].Parent.Left = n.Result.Head;
                }
                else
                {
                    exp.OperatorNodes[j].Parent.Right = n.Result.Head;
                }

                n.Result = new Expression( ExpressionFactory.ConvertToMiddle( exp.Head ) );
                AddConditions( new List<ProveNode> { n } );
            }
        }

        private void AddConditions( List<ProveNode> list )
        {
            foreach ( ProveNode n in list )
            {
                if ( !IsExistResult( n.Result.AfterExpress ) )  //
                {
                    results.Add( n );
                    CreateResult( n );
                }
            }
        }

        private bool IsExistResult( string p )
        {
            foreach ( ProveNode e in results )
            {
                if ( p == e.Result.AfterExpress )
                    return true;
            }
            return false;
        }

    }
}
